$\forall$$T$:Type, $L$:($T$ List).
\\[0ex]no\_repeats($T$;$L$)
\\[0ex]$\Rightarrow$ ($\forall$$A$:Type, $f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$$A$). Inj(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} ;$A$;$f$) $\Rightarrow$ no\_repeats($A$;map($f$;$L$)))